$\forall$${\it the\_es}$:ES, $j$:E.
\\[0ex]($\uparrow$isrcv($j$))
\\[0ex]$\Rightarrow$ (snds(lnk($j$), before(sender($j$),index($j$))) = [] $\in$ ((Msg on lnk($j$)) List))
\\[0ex]$\Rightarrow$ (msgs(lnk($j$);before($j$)) = [] $\in$ (Msg List))